Inference at * 
Iof proof for Lemma wellfounded functionality wrt implies:


  T1,T2:Type, r1:(T1T1), r2:(T2T2).
  (T1 = T2)
   (x,y:T1. {r1(x,y)  r2(x,y)})
   {WellFnd{i}(T1;x,y.r1(x,y))  WellFnd{i}(T2;x,y.r2(x,y))} 

latex

 by ((((Unfolds ``wellfounded guard`` 0) 
CollapseTHEN (UnivCD))) 
CollapseTHENA (
C(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term))) 

latex

C1: 

C1: 1. T1 : Type
C1: 2. T2 : Type
C1: 3. r1 : T1T1
C1: 4. r2 : T2T2
C1: 5. T1 = T2
C1: 6. x,y:T1. r1(x,y)  r2(x,y)
C1: 7. P:(T1). (j:T1. (k:T1. r1(k,j)  P(k))  P(j))  {n:T1. P(n)}
C1: 8. P : T2
C1: 9. j:T2. (k:T2. r2(k,j)  P(k))  P(j)
C1:   n:T2. P(n)
C.

Definitions	t  T, x(s), WellFnd{i}(A;x,y.R(x;y)), x(s1,s2), P  Q, {T}, P  Q, , x:A. B(x)
Lemmas	rev implies wf, guard wf